perm filename ANSWER[P,JRA] blob
sn#139979 filedate 1975-01-11 generic text, type T, neo UTF8
00100
00150 (SETQ UFLG NIL)
00175 (SETQ THMLIST NIL)
00200
00300 (DEFPROP ALLPOS
00400 (LAMBDA (C) (LIST (QUOTE NULL) (LIST (QUOTE CADAR) (CADR C))))
00500 MACRO)
00600
00700 (DEFPROP ALLNEG
00800 (LAMBDA (C) (LIST (QUOTE EQ) (LIST (QUOTE CADAR) (CADR C)) (LIST (QUOTE CDR) (CADR C))))
00900 MACRO)
01000
01100 (DEFPROP ANCESTOR
01200 (LAMBDA (X) (LIST (QUOTE CDDDAR) (CADR X)))
01300 MACRO)
01400
01500 (DEFPROP SEARCH1
01600 (LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) NIL))
01700 MACRO)
01800
01900 (DEFPROP CONST
02000 (LAMBDA (X) (LIST (QUOTE NULL) (LIST (QUOTE CDR) (CADR X))))
02100 MACRO)
02200
02300 (DEFPROP HERE
02400 (LAMBDA (X) (LIST (QUOTE CAAR) (CADR X)))
02500 MACRO)
02600
02700 (DEFPROP VAR
02800 (LAMBDA (L) (LIST (QUOTE NUMBERP) (CADR L)))
02900 MACRO)
03000
03100 (DEFPROP ISCLS
03200 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 1))
03300 MACRO)
03400
03500 (DEFPROP ISCL
03600 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 2))
03700 MACRO)
03800
03900 (DEFPROP ISLIT
04000 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 3))
04100 MACRO)
04200
04300 (DEFPROP ISTRM
04400 (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 4))
04500 MACRO)
04600
04700 (DEFPROP MKWRD
04800 (LAMBDA (L) (LIST (QUOTE CDDAR) (CADR L)))
04900 MACRO)
05000
05100 (DEFPROP NEG
05200 (LAMBDA (X) (LIST (QUOTE EQ) (QUOTE ESCAPE) (LIST (QUOTE CAR) (CADR X))))
05300 MACRO)
05400
05500 (DEFPROP NEGBIT
05600 (LAMBDA (X) (LIST (QUOTE CDDAAR) (CADR X)))
05700 MACRO)
05800
05900 (DEFPROP POS
06000 (LAMBDA (X) (LIST (QUOTE NOT) (LIST (QUOTE NEG) (CADR X))))
06100 MACRO)
06200
06300 (DEFPROP POSBIT
06400 (LAMBDA (X) (LIST (QUOTE CADAAR) (CADR X)))
06500 MACRO)
06600
06700 (DEFPROP SEARCH
06800 (LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) (CADR X)))
06900 MACRO)
07000
07100 (DEFPROP NEGL
07200 (LAMBDA (C) (LIST (QUOTE CADAR) (CADR C)))
07300 MACRO)
00100
00200 (DE VINE(X)(ATOM(CDR(ANCESTOR X))) )
00300
00400 (DEFPROP ALPHABETIC
00500 (LAMBDA(R L)
00600 (PROG NIL
00700 A (COND ((OR (NULL L) (NULL (CAR L))) (RETURN R))
00800 ((NOT (EQ (LENGTH (CDR R)) (LENGTH (CDAR L)))) (GO B))
00900 ((ALPHAV (CDR R) (CDAR L) NIL) (RETURN (CAR L))))
01000 B (SETQ L (CDR L))
01100 (COND (L (GO A)) (T (RETURN NIL)))))
01200 EXPR)
01300
01400 (DEFPROP ALPHAV
01500 (LAMBDA(C1 C2 L)
01600 (PROG NIL
01700 AL1 (COND ((NULL C1) (RETURN T)) ((NEG (CAR C1)) (GO AL3)) ((NOT (EQ (CAAR C1) (CAAR C2))) (RETURN NIL)))
01800 (SETQ L (ANSUNI (CDAR C1) (CDAR C2) L))
01900 AL2 (COND ((NULL L) (RETURN NIL)))
02000 (SETQ C1 (CDR C1))
02100 (SETQ C2 (CDR C2))
02200 (GO AL1)
02300 AL3 (COND ((POS (CAR C2)) (RETURN NIL))
02400 ((EQ (CADAR C1) (CADAR C2)) (SETQ L (ANSUNI (CDDAR C1) (CDDAR C2) L)) (GO AL2)))
02500 (RETURN NIL)))
02600 EXPR)
02700
02800 (DEFPROP ANSPRED
02900 (LAMBDA NIL (ANSPRINT (STAGE1 (ANSWER (CONS LHP RHP)))))
03000 EXPR)
03100
03200 (DEFPROP ANSPRINT
03300 (LAMBDA(L)
03400 (PROG (Z VARL ONO)
03500 (SETQ ONO 0)
03600 B (PRINC (QUOTE /())
03700 (SETQ Z (CDAR L))
03800 A (COND ((NEG (CAR Z)) (PRFPR1 (CDAR Z))) (T (PRFPR1 (CONS ESCAPE (CAR Z)))))
03900 (SETQ Z (CDR Z))
04000 (COND (Z (PRINC (QUOTE / )) (PRINC (QUOTE ∧)) (PRINC (QUOTE / )) (GO A)))
04100 (PRINC (QUOTE /)))
04200 (SETQ L (CDR L))
04300 (COND (L (PRINC (QUOTE / )) (PRINC (QUOTE ∨)) (PRINC (QUOTE / )) (GO B)))
04400 (RETURN NIL)))
04500 EXPR)
04600
04700 (DEFPROP ANSWER
04800 (LAMBDA(L)
04900 (PROG (SUBST TREE Z Z1 Z2 NO* NO1)
05000 (SETQ NO* NO)
05100 (SETQ NO1 NO)
05200 (SETQ Z (ANS1 L))
05300 (SETQ Z (REVERSE (SET3 (RESTORE1 (REVERSE (COPY Z))))))
05400 (SETQ Z1 Z)
05500 B (SETQ Z2 (CAR Z1))
05600 (COND ((VINE Z2) (SETQ BL NIL) (STAND Z2)))
05700 (SETQ Z1 (CDR Z1))
05800 (COND (Z1 (GO B)))
05900 (SETQ TREE Z)
06000 (SETQ Z1 TREE)
06100 (SETQ NO 0)
06200 (SETQ SUBST (LIST NIL))
06300 C (COND ((VINE (CAR TREE)) (GO D)))
06400 (SETQ Z (ANCESTOR (CAR TREE)))
06500 (SETQ Z (RES (CAR Z) (CDR Z) (CAR TREE)))
06600 (STAND1 (CAR TREE) (CDR Z))
06700 (ST2 (CAR Z) SUBST)
06800 D (SETQ TREE (CDR TREE))
06900 (COND (TREE (GO C)))
07000 (SETQ NO NO1)
07100 (RETURN (NEGTHM Z1 (CDR SUBST)))))
07200 EXPR)
07300
07400 (DEFPROP ANSWER
07500 (NIL ALPHABETIC
07600 ALPHAV
07700 ANSPRED
07800 ANSPRINT
07900 ANSWER
08000 IN
08100 NEGTHM
08200 SUBS
08300 ANSUNI
08400 ANS1
08500 COLLECT
08600 RES
08700 RES1
08800 STAGE1
08900 STAND
09000 STAND1
09100 ST2)
09200 VALUE)
09300
09400 (DEFPROP IN
09500 (LAMBDA(T1 S)
09600 (PROG (Z)
09700 A (COND ((NULL S) (RETURN NIL)))
09800 (SETQ Z (CAR S))
09900 (COND ((EQUAL (CDR Z) T1) (RETURN (CAR Z))))
10000 (SETQ S (CDR S))
10100 (GO A)))
10200 EXPR)
10300
10400 (DEFPROP NEGTHM
10500 (LAMBDA(L S)
10600 (PROG (Z)
10700 (COND ((NULL L) (RETURN (LIST NIL))))
10800 A1 (COND ((NULL L) (RETURN Z))
10900 ((AND (ATOM (CAR (ANCESTOR (CAR L)))) (EQ THEOREMNAME (CAR (ANCESTOR (CAR L)))))
11000 (SETQ Z (CONS (SUBS S (CAR L)) Z))))
11100 (SETQ L (CDR L))
11200 (GO A1)))
11300 EXPR)
11400
11500 (DEFPROP SUBS
11600 (LAMBDA(S C)
11700 (PROG (Z) (SETQ Z C) A (SETQ C (CDR C)) (COND ((NULL C) (RETURN Z))) (RPLACA C (SUBS3T S (CAR C))) (GO A)))
11800 EXPR)
11900
12000 (DEFPROP ANSUNI
12100 (LAMBDA(C D L)
12200 (PROG (Z1 Z2 Z3)
12300 UN2 (SETQ Z2 (CAR D))
12400 (SETQ Z1 (SETQ Z3 (CAR C)))
12500 (COND
12600 ((AND (VAR Z2) (VAR Z1)) (SETQ Z3 (SEARCH1 Z1 L))
12700 (COND ((NULL Z3) (SETQ L (CONS (CONS Z1 Z2) L)) (GO UN1))
12800 ((VAR Z3) (COND ((EQ Z3 Z2) (GO UN1)) (T (RETURN NIL)))))))
12900 (COND ((OR (VAR Z1) (VAR Z2)) (RETURN NIL))
13000 ((CONST Z2) (COND ((EQ (CAR Z2) (CAR Z3)) (GO UN1)) (T (RETURN NIL))))
13100 ((EQ (CAR Z2) (CAR Z3)) (SETQ C (APPEND (CDR Z3) (CDR C)))
13200 (SETQ D (APPEND (CDR Z2) (CDR D)))
13300 (GO UN2))
13400 (T (RETURN NIL)))
13500 UN1 (SETQ C (CDR C))
13600 (COND (C (SETQ D (CDR D)) (GO UN2)))
13700 (COND (L (RETURN L)) (T (RETURN (LIST (CONS 64 64)))))))
13800 EXPR)
13900
14000 (DEFPROP ANS1
14100 (LAMBDA(L)
14200 (PROG (Z Z2 Z3 Z4 Z5 L1 N)
14300 (SETQ N 1)
14400 (SETQ L (LIST (CONS (CONS NIL (CONS NIL (CONS 0 L))) (QUOTE ((ANS (A)))))))
14500 B (SETQ Z2 (CAAR L))
14600 (SETQ Z3 (LENGTH (CDAR L)))
14700 (COND ((NULL (CADR Z2)) (SETQ Z4 NIL))
14800 (T
14900 (SETQ Z4
15000 (PROG (Z Z1 N)
15100 (SETQ N 0)
15200 (SETQ Z1 (CDAR L))
15300 (SETQ Z (CADR Z2))
15400 A (COND ((EQ Z Z1) (RETURN N)))
15500 (SETQ Z1 (CDR Z1))
15600 (SETQ N (ADD1 N))
15700 (GO A)))))
15800 (SETQ Z (CDDDR Z2))
15900 (COND ((ATOM (CDR Z))
16000 (COND ((NOT (ATOM (CAR Z))) (RPLACD (LAST L) (LIST (CAAR Z) (CDAR Z)))
16100 (SETQ Z5 (CONS N (ADD1 N)))
16200 (SETQ N (ADD1 (ADD1 N))))
16300 (T (SETQ Z5 (LIST Z)))))
16400 (T (RPLACD (LAST L) (LIST (CAR Z) (CDR Z)))
16500 (SETQ Z5 (CONS N (ADD1 N)))
16600 (SETQ N (ADD1 (ADD1 N)))))
16700 (SETQ Z (CONS Z3 (CONS Z4 (CONS 0 Z5))))
16800 (SETQ L1 (CONS (CONS Z (CDAR L)) L1))
16900 (SETQ L (CDR L))
17000 (COND (L (GO B)))
17100 (RETURN L1)))
17200 EXPR)
17300
17400 (DEFPROP COLLECT
17500 (LAMBDA(L S)
17600 (PROG (Z)
17700 A (COND ((NULL L) (RETURN S))
17800 ((VAR (CAR L)) NIL)
17900 ((SETQ Z (IN (CAR L) S)) (RPLACA L Z))
18000 ((MEMBER (CAAR L) THMLIST)
18100 (RPLACA L (CAAR (SETQ S (CONS (CONS (SETQ NEWV (SUB1 NEWV)) (CAR L)) S)))))
18200 (T (SETQ S (COLLECT (CDAR L) S))))
18300 (SETQ L (CDR L))
18400 (GO A)))
18500 EXPR)
18600
18700 (DEFPROP RES
18800 (LAMBDA(C D R)
18900 (COND ((OR (ALLNEG D) (ALLPOS C)) (RES1 C D R))
19000 ((OR (ALLPOS D) (ALLNEG C)) (RES1 D C R))
19100 (T (NCONC (RES1 C D R) (RES1 D C R)))))
19200 EXPR)
19300
19400 (DEFPROP RES1
19500 (LAMBDA(C D R)
19600 (PROG (CB DB DB1 YC YD YD1 Z X Y RES)
19700 (COND ((EQ C D) (RETURN NIL)))
19800 (SETQ YC (CDR C))
19900 (SETQ CB (POSBIT C))
20000 (SETQ YD1 (NEGL D))
20100 (SETQ DB1 (NEGBIT D))
20200 (SETQ DB DB1)
20300 (SETQ YD YD1)
20400 RES1 (SETQ X (CAR YC))
20500 (COND ((NEG X) (RETURN NIL)))
20600 (SETQ Y (CAR YD))
20700 (COND ((ORDERP (CAR X) (CADR Y)) (GO RES3)) ((NOT (EQ (CAR X) (CADR Y))) (GO RES4)))
20800 (SETQ YD1 YD)
20900 (SETQ DB1 DB)
21000 (GO RES2A)
21100 RES2 (SETQ Y (CAR YD))
21200 (COND ((NOT (EQ (CAR X) (CADR Y))) (GO RES3A)))
21300 RES2A
21400 (COND ((NOT (UNIFAB (CAR CB) (CAR DB))) (GO RES2B)))
21500 (SETQ Z (UNIFY (CDR X) (CDDR Y)))
21600 (COND
21700 (Z (SETQ PARRES NIL)
21800 (COND ((SETQ RES (ALPHABETIC R (UNION (CDR Z) C D X Y))) (RETURN (CONS (CDR Z) RES))) (T NIL))))
21900 RES2B
22000 (SETQ YD (CDR YD))
22100 (SETQ DB (CDR DB))
22200 (COND (YD (GO RES2)))
22300 RES3A
22400 (SETQ DB DB1)
22500 (SETQ YD YD1)
22600 RES3 (SETQ YC (CDR YC))
22700 (SETQ CB (CDR CB))
22800 (COND (YC (GO RES1)))
22900 (RETURN NIL)
23000 RES4 (SETQ YD (CDR YD))
23100 (SETQ DB (CDR DB))
23200 (COND (YD (GO RES1)))
23300 (GO RES3A)))
23400 EXPR)
23500
23600 (DEFPROP STAGE1
23700 (LAMBDA(L)
23800 (PROG (Z Z1 S NEWV)
23900 (SETQ Z L)
24000 (SETQ NEWV -1)
24100 B (SETQ Z1 (CDAR Z))
24200 A (COND ((NEG (CAR Z1)) (SETQ S (COLLECT (CDDAR Z1) S))) (T (SETQ S (COLLECT (CDAR Z1) S))))
24300 (SETQ Z1 (CDR Z1))
24400 (COND (Z1 (GO A)))
24500 (SETQ Z (CDR Z))
24600 (COND (Z (GO B)))
24700 (RETURN L)))
24800 EXPR)
24900
25000 (DEFPROP STAND
25100 (LAMBDA (X) (PROG (Z) (SETQ Z (CDR X)) A (UPIT (CAR Z)) (SETQ Z (CDR Z)) (COND (Z (GO A))) (RETURN X)))
25200 EXPR)
25300
25400 (DEFPROP STAND1
25500 (LAMBDA(OL NE)
25600 (PROG (Z Z1)
25700 (RPLACA (CAAR OL) (CAAR NE))
25800 (SETQ Z (CDR OL))
25900 (SETQ Z1 (CDR NE))
26000 A (RPLACA Z (CAR Z1))
26100 (SETQ Z (CDR Z))
26200 (SETQ Z1 (CDR Z1))
26300 (COND (Z (GO A)))
26400 (RETURN NIL)))
26500 EXPR)
26600
26700 (DEFPROP ST2
26800 (LAMBDA(L1 L)
26900 (PROG (L2) A (COND ((NULL L1) (RETURN NIL))) (SUBS2T (CDAR L1) (CAAR L1) L) (SETQ L1 (CDR L1)) (GO A)))
27000 EXPR)
00100
00200
00600
00700 (DEFPROP RESTORE
00800 (LAMBDA(IL)
00900 (PROG (ZZ) (EVAL (CONS (QUOTE INPUT) IL)) (INC T) (SETQ ZZ (RESTORE1 (READ))) (INC NIL) (RETURN (SET3 ZZ))))
01000 FEXPR)
01100
01200 (DEFPROP RESTORE1
01300 (LAMBDA(L)
01400 (PROG (Z2 Z L1 L2 Z1 N)
01500 (SETQ L1 L)
01600 (SETQ N 0)
01700 D (SETQ L2 (CONS (CONS N (CAR L)) L2))
01800 (SETQ L (CDR L))
01900 (SETQ N (ADD1 N))
02000 (COND (L (GO D)))
02100 (SETQ L L1)
02200 E (SETQ Z (CAAR L1))
02300 (SETQ Z1 (CADR Z))
02400 (COND ((NULL Z1) (GO A)))
02500 (SETQ Z2 (CDAR L1))
02600 B (COND ((ZEROP Z1) (RPLACA (CDR Z) Z2) (GO A)))
02700 (SETQ Z1 (SUB1 Z1))
02800 (SETQ Z2 (CDR Z2))
02900 (GO B)
03000 A (SETQ Z1 (CDDDR Z))
03100 (COND ((NULL (CDR Z1)) (RPLACD (CDDR Z) (CAR Z1)) (GO C)) ((NULL (CAR Z1)) (SETQ Z1 (CDR Z1))))
03200 F (RPLACA Z1 (CDR (ASSOC (CAR Z1) L2)))
03300 (RPLACD Z1 (CDR (ASSOC (CDR Z1) L2)))
03400 C (SETQ L1 (CDR L1))
03500 (COND (L1 (GO E)))
03600 (RETURN L)))
03700 EXPR)
03800
03900 (DEFPROP RESTART
04000 (LAMBDA(X)
04100 (PROG (ZZ TIME1)
04200 (EVAL (CONS (QUOTE INPUT) X))
04300 (INC T)
04400 (SETQ ZZ (RESTORE1 (READ)))
04500 (SETQ STRAT (READ))
04600 (SETQ COND (READ))
04700 (INC NIL)
04800 (SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
04900 (RETURN (ATTEMPT (CONS ZZ (FIXSET ZZ)) STRAT COND))))
05000 FEXPR)
05100
05200 (DEFPROP SAVE
05300 (LAMBDA(CL)
05400 (PROG (L)
05500 (SETQ L (SAVE1 (EVAL (CADDR CL))))
05600 (EVAL (CONS (QUOTE OUTPUT) (LIST (CAR CL) (CADR CL))))
05700 (OUTC T T)
05800 (PRINT L)
05900 (PRINT STRAT)
06000 (PRINT COND)
06100 (OUTC NIL T)
06200 (RETURN NIL)))
06300 FEXPR)
06400
06500 (DEFPROP SAVE1
06600 (LAMBDA(L)
06700 (PROG (L1 N ASLST CLST Z Z2 Z3 Z4 Z5)
06800 (SETQ N 0)
06900 (SETQ Z L)
07000 A (SETQ ASLST (CONS (CONS (CAR L) N) ASLST))
07100 (SETQ L (CDR L))
07200 (SETQ N (ADD1 N))
07300 (COND (L (GO A)))
07400 (SETQ CLST (LAST Z))
07500 (SETQ L Z)
07600 B (SETQ Z2 (CAAR L))
07700 (COND ((NULL (CAR Z2)) (SETQ Z3 NIL)) (T (SETQ Z3 (CAAR Z2))))
07800 (COND ((NULL (CADR Z2)) (SETQ Z4 NIL))
07900 (T
08000 (SETQ Z4
08100 (PROG (Z Z1 N)
08200 (SETQ N 0)
08300 (SETQ Z1 (CDAR L))
08400 (SETQ Z (CADR Z2))
08500 A (COND ((EQ Z Z1) (RETURN N)))
08600 (SETQ Z1 (CDR Z1))
08700 (SETQ N (ADD1 N))
08800 (GO A)))))
08900 (SETQ Z (CDDDR Z2))
09000 (COND ((ATOM (CDR Z))
09100 (COND ((NOT (ATOM (CAR Z))) (SETQ Z5 (UNWIND (CAAR Z) (CDAR Z) CLST ASLST N))
09200 (SETQ N (CDR Z5))
09300 (SETQ Z5 (CONS NIL (CAR Z5))))
09400 (T (SETQ Z5 (LIST Z)))))
09500 (T (SETQ Z2 (UNWIND (CAR Z) (CDR Z) CLST ASLST N)) (SETQ Z5 (CAR Z2)) (SETQ N (CDR Z2))))
09600 (SETQ Z (CONS Z3 (CONS Z4 (CONS 0 Z5))))
09700 (SETQ L1 (CONS (CONS Z (CDAR L)) L1))
09800 C (SETQ L (CDR L))
09900 (COND (L (GO B)))
10000 (RPLACD CLST NIL)
10100 (RETURN (REVERSE L1))))
10200 EXPR)
10300
10400 (DEFPROP NAME
10500 (NIL REENTER RESTORE RESTORE1 RESTART SAVE SAVE1 NAME)
10600 VALUE)